$LOAD_PATH.unshift File.join(File.dirname(__FILE__),'../..','ext_pr1/lib')
require 'ext_pr1_v4'

class Object
   def clock?()     false end
   def clock_sec?() false end
   def clock_12?()  false end
   def clock_24?()  false end
   def clock_am?()  false end
   def clock_pm?()  false end
   def sec_day?()   false end
   def sec?()       false end
   def min?()       false end
   def hour12?()    false end
   def hour24?()    false end
   def halve()      false end
end

class Symbol
   def halve?()
      ((self == :AM) or (self == :PM))
   end
end

class Integer
   def day_sec?() self.in?(0...(Clock::DAY24_IN_SEC))   end
   def sec?()     self.in?(0...(Clock::MIN_IN_SEC))     end
   def min?()     self.in?(0...(Clock::HOUR_IN_MIN))    end
   def hour12?()  self.in?(0...(Clock::DAY_IN_HOURS12)) end
   def hour24?()  self.in?(0...(Clock::DAY_IN_HOURS24)) end
end

#####################################################################
## CLOCK
class Clock
   # CONSTANTS
   DAY_IN_HOURS12 = 12
   DAY_IN_HOURS24 = 24
   HOUR_IN_MIN = 60
   MIN_IN_SEC = 60
   ZERO_SEC = 0
   HOUR_IN_SEC = HOUR_IN_MIN * MIN_IN_SEC
   DAY24_IN_SEC = HOUR_IN_SEC * DAY_IN_HOURS24
   DAY12_IN_SEC = HOUR_IN_SEC * DAY_IN_HOURS12

   # CREATION
   def self.[](*args) check_inv(self.new(*args)) end
   def initialize() abstract end
   def invariant?() abstract end

   # SELEKTOREN
   def hour24_()  abstract   end
   def hour12_()  abstract   end
   def halve()    abstract   end
   def min()      abstract   end
   def sec()      abstract   end
   def day_sec_() abstract   end

   # TYPPRÄDIKATE
   def clock?() true end
   def clock_pm?()  (self.to_clock_sec.day_sec) % Clock::DAY24_IN_SEC >= DAY12_IN_SEC   end
   def clock_am?()  (not self.clock_pm?) end

   # EQUIVALENCES
   def == (o) equal?(o) or (o.clock? and to_clock_sec.day_sec == o.to_clock_sec.day_sec) end

   # KONVERSIONEN 
   def to_clock_sec() abstract end
   def to_clock_24()  abstract end
   def to_clock_12()  abstract end
   def to_s()         abstract end
   def clock_zero()   abstract end

   # OPERATIONEN
   def clock_succ()     abstract end
   def clock_pred()     abstract end
   def clock_add(clock) abstract end
   def clock_sub(clock) abstract end
   def invers()         abstract end
   def -@() self.invers end
   def +(clock) self.clock_add(clock) end
   def -(clock) self.clock_sub(clock) end
end

#####################################################################
## CLOCK24
class Clock24 < Clock
   # CREATION
   def initialize(hour,min,sec) @hour = hour; @min = min; @sec = sec end
   def invariant?()   self.hour24_.hour24? and self.min.min? and self.sec.sec?   end

   # SELEKTOREN
   def hour24_() @hour end
   def hour12_() self.to_clock_sec.to_clock_12.hour   end
   def halve()   self.to_clock_sec.to_clock12.halve   end
   def min()     @min end
   def sec()     @sec end

   # TYPPRÄDIKATE
   def clock_24?() true end

   # STRING
   def to_s() 'Clock24'+'['+(self.hour24_.to_s)+':'+(self.min_.to_s)+':'+(self.sec_.to_s)+']' end

   # KONVERSIONEN
   # Clock24 => ClockSec
   def to_clock_sec() ClockSec[((self.hour24_ * Clock::HOUR_IN_SEC) + (self.min * Clock::MIN_IN_SEC) + self.sec)] end
   # Clock24 => Clock24
   def to_clock_24() self end
   # Clock24 => Clock12
   def to_clock_12() self.to_clock_sec.to_clock_12 end
   def clock_zero() self.to_clock_sec.clock_zero.to_clock_12 end
   
   # OPERATIONS
   # Clock24 x Clock24 => Clock24 | Clock24 => Clock24
   def clock_add(c) check_pre(c.clock?); self.to_clock_sec.clock_add(c).to_clock_24 end
   def clock_sub(c) check_pre(c.clock?); self.to_clock_sec.clock_sub(c).to_clock_24 end
   def clock_pred() self.to_clock_sec.clock_pred.to_clock_24 end
   def clock_succ() self.to_clock_sec.clock_succ.to_clock_24 end
   def invers() self.to_clock_sec.invers.to_clock_24 end
end

#####################################################################
## CLOCK12
class Clock12 < Clock
   # CREATION
   def initialize(halve,hour,min,sec)  @halve = halve; @hour = hour; @min = min; @sec = sec   end
   def invariant?()  self.halve.halve? and self.hour12_.hour12? and self.min.min? and self.sec.sec?   end

   # SELEKTOREN
   def hour24_() self.to_clock_24.hour   end
   def hour12_() @hour  end
   def min()     @min end
   def sec()     @sec end
   def halve()   @halve end

   # TYPPRÄDIKATE
   def clock_12?() true end

   # STRING
   def to_s() 'Clock12'+'['+(self.halve.to_s)+':'+(self.hour12_.to_s)+':'+(self.min.to_s)+':'+(self.sec.to_s)+']' end

   # CONVERSIONS
   # Clock12 -> ClockSec
   def to_clock_sec()
      if self.halve == :PM then ClockSec[(((self.hour12_ + Clock::DAY_IN_HOURS12)*Clock::HOUR_IN_SEC) + (self.min * Clock::MIN_IN_SEC) + self.sec)]
     else                       ClockSec[(((self.hour12_)*Clock::HOUR_IN_SEC) + (self.min * Clock::MIN_IN_SEC) + self.sec)] end
   end
   #Clock12->Clock24
   def to_clock_24() self.to_clock_sec.to_clock_24 end
   #Clock12->Clock12
   def to_clock_12() self end
   def clock_zero() self.to_clock_sec.clock_zero.to_clock_12 end
   
   # OPERATIONS
   # Clock12 x Clock12 => Clock12 | Clock12 => Clock12
   def clock_add(c) check_pre(c.clock?); self.to_clock_sec.clock_add(c).to_clock_12 end
   def clock_sub(c) check_pre(c.clock?); self.to_clock_sec.clock_sub(c).to_clock_12 end
   def clock_pred() self.to_clock_sec.clock_pred.to_clock_12 end
   def clock_succ() self.to_clock_sec.clock_succ.to_clock_12 end
   def invers() self.to_clock_sec.invers.to_clock_12 end
end

#####################################################################
## CLOCK_SEC
class ClockSec < Clock
   # CREATION
   def initialize(day_sec) @day_sec = day_sec end
   def invariant?() self.day_sec.day_sec? end

   # SELECTORS
   def day_sec() @day_sec end

   # TYPE PREDS
   def clock_sec?() true end

   # STRING
   def to_s() 'ClockSec'+'['+(self.day_sec.to_s)+']' end

   ## CONVERSIONS
   # ClockSec -> ClockSec
   def to_clock_sec() self end
   
   def to_clock_s(s) ClockSec[s >= Clock::DAY24_IN_SEC ? Clock::DAY24_IN_SEC-s : s<ZERO_SEC ? Clock::DAY24_IN_SEC+s : s] end

   # ClockSec -> clock24
   def to_clock_24()
      s = @day_sec.divmod(MIN_IN_SEC)
      m = s[0].divmod(HOUR_IN_MIN)
      h = m[0].divmod(DAY_IN_HOURS24)
      Clock24[h[1],m[1],s[1]]
   end

   # ClockSec -> Clock12
   def to_clock_12()
      s = @day_sec.divmod(MIN_IN_SEC)
      m = s[0].divmod(HOUR_IN_MIN)
      h = m[0].divmod(DAY_IN_HOURS12)
      Clock12[ ( h[0] > 0 ? :PM : :AM ),h[1],m[1],s[1]]
   end
   
   # OPERATIONS
   # ClockSec x ClockSec => ClockSec |  ClockSec => ClockSec
   def clock_add(c) check_pre(c.clock?); to_clock_s(self.day_sec + c.to_clock_sec.day_sec) end
   def clock_sub(c) check_pre(c.clock?); to_clock_s(self.day_sec - c.to_clock_sec.day_sec) end
   def clock_pred() to_clock_s(self.day_sec-1) end
   def clock_succ() to_clock_s(self.day_sec+1) end
   def clock_zero() to_clock_s(ZERO_SEC) end
   def invers() to_clock_s(Clock::DAY24_IN_SEC-self.day_sec) end
end
